Boolean Satisfiability (SAT) is a problem that has both academic and practical significance. For example, in industry, techniques for demonstrating Boolean Satisfiability are used to prove the correctness of digital logic circuits and for many other purposes. Although numerous algorithms for proving Boolean Satisfiability of formulas have been proposed and implemented, none of them can operate in polynomial time.